<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Notifications | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Notifications</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="notifications-and-shared-memory">Notifications and shared memory</h1>

<p>This tutorial covers notification objects.</p>

<p>You will learn how to:</p>
<ol>
  <li>Set up shared memory between tasks.</li>
  <li>Use notification objects for synchronisation between tasks.</li>
  <li>Use badges to differentiate notifications.</li>
</ol>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/capabilities">Capabilities tutorial</a></li>
  <li><a href="/Tutorials/mapping">Mapping tutorial</a></li>
  <li><a href="/Tutorials/threads">Threads tutorial</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> notifications
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>notifications_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> notifications
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>notifications_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="capdl-loader">CapDL Loader</h2>

<p>This tutorial uses the <em>capDL loader</em>, a root task which allocates statically
 configured objects and capabilities.</p>

<details>
  <summary>Get CapDL</summary>
  <p>The capDL loader parses
a static description of the system and the relevant ELF binaries.
It is primarily used in <a href="https://docs.sel4.systems/CAmkES/">Camkes</a> projects
but we also use it in the tutorials to reduce redundant code.
The program that you construct will end up with its own CSpace and VSpace, which are separate
from the root task, meaning CSlots like <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadVSpace</code> have no meaning
in applications loaded by the capDL loader.</p>

  <p>More information about CapDL projects can be found <a href="https://docs.sel4.systems/CapDL.html">here</a>.</p>

  <p>For this tutorial clone the <a href="https://github.com/sel4/capdl">CapDL repo</a>. This can be added in a directory that is adjacent to the tutorials-manifest directory.</p>
</details>

<h2 id="background">Background</h2>

<p>Notifications allow processes to send asynchronous signals to each other, and are primarily used for interrupt handling
and to synchronise access to shared data buffers.</p>

<h3 id="notification-objects">Notification objects</h3>

<p>Signals are sent and received with invocations on capabilities to notification objects.
A notification object consists of a data word, which acts as an array of binary semaphores, and a queue of
TCBs waiting for notifications.</p>

<p>Notification objects can be in three states:</p>
<ul>
  <li>Waiting - there are TCBs queued on this notification waiting for it to be signalled.</li>
  <li>Active - TCBs have signalled data on this notification,</li>
  <li>Idle - no TCBs are queued and no TCBs have signalled this object since it was last set to idle.</li>
</ul>

<h4 id="signalling">Signalling</h4>

<p>When a task signals a notification object (using <code class="language-plaintext highlighter-rouge">seL4_Signal</code>), what occurs depends on the state of the object:</p>
<ul>
  <li>Idle - the data word is set to the badge of the capability used to send the signal, and the object is converted
 to active.</li>
  <li>Active - the badge of the capability used to signal the notification object is bitwise-orred with the notifications data word.</li>
  <li>Waiting - the head of the queue of TCBs is woken and the badge sent to that TCB. If the queue is empty, the notification
object is transitioned to idle.</li>
</ul>

<p>In this way notification objects can be seen as a binary array of semaphores - if the signallers all use a
different bit in the badge, they can set different badge bits and waiters can observe which bits have been set.</p>

<h4 id="waiting">Waiting</h4>

<p>Tasks can wait on a notification object using <code class="language-plaintext highlighter-rouge">seL4_Wait</code>, which does the following:</p>

<ul>
  <li>Idle - the TCB is queued, and the notification transitioned to waiting.</li>
  <li>Active - the TCB receives the data word, the data word is reset to 0 and the notification transitioned to idle,</li>
  <li>Waiting - the TCB is appended to the queue.</li>
</ul>

<h4 id="polling">Polling</h4>

<p>Notification objects can also be polled with <code class="language-plaintext highlighter-rouge">seL4_Poll</code>, which is a non-blocking version of <code class="language-plaintext highlighter-rouge">seL4_Wait</code> that returns
immediately regardless of the state.</p>

<h2 id="interrupts-and-ipc">Interrupts and IPC</h2>

<p>Notification objects can be used to receive signals of interrupt delivery, and can also be bound to TCBs
such that signals and IPC can be received by the same thread. This is explained in more detail in the
timer tutorial. <!--TODO link to timer tutorial --></p>

<h2 id="exercises">Exercises</h2>

<p>These exercises guide you through a basic producer consumer set up using notifications and shared memory. The
tutorial uses the capDL loader, and already has 2 producer processes (<code class="language-plaintext highlighter-rouge">producer_1.c</code> and <code class="language-plaintext highlighter-rouge">producer_2</code>) and 1 consumer
 process running (<code class="language-plaintext highlighter-rouge">consumer.c</code>). Each has access to a number of capabilities.</p>

<p>Each producer shares a buffer with the consumer, and the consumer processes data from both producers when it is
available.</p>

<p>When you start the tutorial, the output will look something like this:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
Waiting for producer
</code></pre></div></div>
<h3 id="set-up-shared-memory">Set up shared memory</h3>

<p>Both producers start and block immediately, waiting for the consumer to send an IPC with the address of the shared
mapping. We provide code below that sets up the shared page between producer 1 and the consumer:</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* set up shared memory for consumer 1 */</span>
    <span class="cm">/* first duplicate the cap */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Copy</span><span class="p">(</span><span class="n">cnode</span><span class="p">,</span> <span class="n">mapping_1</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                          <span class="n">cnode</span><span class="p">,</span> <span class="n">buf1_frame_cap</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span> <span class="n">seL4_AllRights</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IFERR</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to copy cap"</span><span class="p">);</span>
    <span class="cm">/* now do the mapping */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_ARCH_Page_Map</span><span class="p">(</span><span class="n">mapping_1</span><span class="p">,</span> <span class="n">producer_1_vspace</span><span class="p">,</span> <span class="n">BUF_VADDR</span><span class="p">,</span>
                               <span class="n">seL4_AllRights</span><span class="p">,</span> <span class="n">seL4_ARCH_Default_VMAttributes</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IFERR</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to map frame"</span><span class="p">);</span>
</code></pre></div></div>

<p>However, we do not map the second buffer in, so producer 2 crashes immediately.</p>

<p><strong>Exercise</strong> Understand the above code, and create a second shared page between <code class="language-plaintext highlighter-rouge">producer_2</code> and <code class="language-plaintext highlighter-rouge">consumer</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// TODO share buf2_frame_cap with producer_2</span>

</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* set up shared memory for producer 2 */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Copy</span><span class="p">(</span><span class="n">cnode</span><span class="p">,</span> <span class="n">mapping_2</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                            <span class="n">cnode</span><span class="p">,</span> <span class="n">buf2_frame_cap</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span> <span class="n">seL4_AllRights</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IFERR</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to copy cap"</span><span class="p">);</span>
   <span class="cm">/* now do the mapping */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_ARCH_Page_Map</span><span class="p">(</span><span class="n">mapping_2</span><span class="p">,</span> <span class="n">producer_2_vspace</span><span class="p">,</span> <span class="n">BUF_VADDR</span><span class="p">,</span>
                               <span class="n">seL4_AllRights</span><span class="p">,</span> <span class="n">seL4_ARCH_Default_VMAttributes</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IFERR</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to map frame"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>Whether this is successful will be visible after the next exercise when the consumers access their buffers. If the shared page setup for producer 2 is not correct, it will fail with a vm fault.</p>

<h3 id="signal-the-producers-to-go">Signal the producers to go</h3>

<p>At this point, both producers are waiting on the <code class="language-plaintext highlighter-rouge">empty</code> notification for a signal that the buffer is ready
to be written to.</p>

<p><strong>Exercise</strong> signal both producers via the <code class="language-plaintext highlighter-rouge">buf1_empty</code> and <code class="language-plaintext highlighter-rouge">buf2_empty</code> notification objects.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// TODO signal both producers</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_Signal</span><span class="p">(</span><span class="n">buf1_empty</span><span class="p">);</span>
    <span class="n">seL4_Signal</span><span class="p">(</span><span class="n">buf2_empty</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="differentiate-signals">Differentiate signals</h3>

<p>Now you should see something like the following:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
Waiting for producer
2: produce
1: produce
Got badge: 2
Got badge: 1
</code></pre></div></div>

<p>At this point, the consumer should consume data from the appropriate buffer(s) and signal to the appropriate consumer(s)
that the buffer is empty again. The capability to the <code class="language-plaintext highlighter-rouge">full</code> notification object has already been badged: <code class="language-plaintext highlighter-rouge">producer_1</code>s
copy has a badge of <code class="language-plaintext highlighter-rouge">0b1</code> and <code class="language-plaintext highlighter-rouge">producer_2</code> a badge of <code class="language-plaintext highlighter-rouge">0b10</code>. By checking the bits in the badge, you can see
which of the producers (it may be both) has produced data.</p>

<p><strong>Exercise</strong> Check the badge and signal the empty notification for the producers according to the bits set in the badge
 value.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// TODO, use the badge to check which producer has signalled you, and signal it back. Note that you</span>
    <span class="c1">// may recieve more than 1 signal at a time.</span>

</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        <span class="k">if</span> <span class="p">(</span><span class="n">badge</span> <span class="o">&amp;</span> <span class="mi">0</span><span class="n">b01</span><span class="p">)</span> <span class="p">{</span>
            <span class="n">assert</span><span class="p">(</span><span class="o">*</span><span class="n">buf1</span> <span class="o">==</span> <span class="mi">1</span><span class="p">);</span>
            <span class="o">*</span><span class="n">buf1</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
            <span class="n">seL4_Signal</span><span class="p">(</span><span class="n">buf1_empty</span><span class="p">);</span>
        <span class="p">}</span>
        <span class="k">if</span> <span class="p">(</span><span class="n">badge</span> <span class="o">&amp;</span> <span class="mi">0</span><span class="n">b10</span><span class="p">)</span> <span class="p">{</span>
            <span class="n">assert</span><span class="p">(</span><span class="o">*</span><span class="n">buf2</span> <span class="o">==</span> <span class="mi">2</span><span class="p">);</span>
            <span class="o">*</span><span class="n">buf2</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
            <span class="n">seL4_Signal</span><span class="p">(</span><span class="n">buf2_empty</span><span class="p">);</span>
        <span class="p">}</span>
</code></pre></div>  </div>
</details>

<p>At this point, you should see signals from both producers being processed, and the final <code class="language-plaintext highlighter-rouge">Success!</code> message printed.</p>

<h3 id="further-exercises">Further exercises</h3>

<p>That’s all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
to become more familiar with IPC.</p>

<ul>
  <li>Create a counting semaphore implementation using notification objects.</li>
  <li>Create a bounded-buffer producer consumer with a buffer size greater than 1.</li>
</ul>



<p style="text-align: right;">

      Next: <a href="/Tutorials/interrupts">Interrupts</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/notifications/notifications.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/notifications/notifications.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#capdl-loader">CapDL Loader</a></li>
<li class="toc-entry toc-h2"><a href="#background">Background</a>
<ul>
<li class="toc-entry toc-h3"><a href="#notification-objects">Notification objects</a>
<ul>
<li class="toc-entry toc-h4"><a href="#signalling">Signalling</a></li>
<li class="toc-entry toc-h4"><a href="#waiting">Waiting</a></li>
<li class="toc-entry toc-h4"><a href="#polling">Polling</a></li>
</ul>
</li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#interrupts-and-ipc">Interrupts and IPC</a></li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#set-up-shared-memory">Set up shared memory</a></li>
<li class="toc-entry toc-h3"><a href="#signal-the-producers-to-go">Signal the producers to go</a></li>
<li class="toc-entry toc-h3"><a href="#differentiate-signals">Differentiate signals</a></li>
<li class="toc-entry toc-h3"><a href="#further-exercises">Further exercises</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/notifications.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/notifications.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
